$\vdash$  $\forall$$A$, $B$:Type, $x$:($A$ + $B$). ($\uparrow$isl($x$)) $\Rightarrow$ (outl($x$) $\in$ $A$)